Nuprl Lemma : all_functionality_wrt_implies
12,41
postcript
pdf
S
,
T
:Type,
P
,
Q
:(
S
). (
S
=
T
)
(
z
:
S
. {
P
(
z
)
Q
(
z
)})
{(
x
:
S
.
P
(
x
))
(
y
:
T
.
Q
(
y
))}
latex
ProofTree
Definitions
t
T
,
x
(
s
)
,
{
T
}
,
P
Q
,
,
x
:
A
.
B
(
x
)
origin
S, T:Type, P, Q:(S
). (S = T) 
(z:S. {P(z) Q(z)}) {(x:S. P(x)) (y:T. Q(y))}
S, T:Type, P, Q:(S). (S = T) (z:S. {P(z) Q(z)}) {(x:S. P(x)) (y:T. Q(y))}
T Qx:A. B(x)